plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
↳ QTRS
↳ DependencyPairsProof
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
LT(s(x), s(y)) → LT(x, y)
IF(true, b, c, x, y) → PLUS(x, y)
FIBITER(b, c, x, y) → LT(c, b)
FIBITER(b, c, x, y) → IF(lt(c, b), b, c, x, y)
IF(true, b, c, x, y) → FIBITER(b, s(c), y, plus(x, y))
FIB(x) → FIBITER(x, 0, 0, s(0))
PLUS(s(x), y) → PLUS(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LT(s(x), s(y)) → LT(x, y)
IF(true, b, c, x, y) → PLUS(x, y)
FIBITER(b, c, x, y) → LT(c, b)
FIBITER(b, c, x, y) → IF(lt(c, b), b, c, x, y)
IF(true, b, c, x, y) → FIBITER(b, s(c), y, plus(x, y))
FIB(x) → FIBITER(x, 0, 0, s(0))
PLUS(s(x), y) → PLUS(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
LT(s(x), s(y)) → LT(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LT(s(x), s(y)) → LT(x, y)
The value of delta used in the strict ordering is 1.
POL(s(x1)) = 1 + x_1
POL(LT(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS(s(x), y) → PLUS(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(x, y)
The value of delta used in the strict ordering is 8.
POL(PLUS(x1, x2)) = (2)x_1
POL(s(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
FIBITER(b, c, x, y) → IF(lt(c, b), b, c, x, y)
IF(true, b, c, x, y) → FIBITER(b, s(c), y, plus(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fib(x) → fibiter(x, 0, 0, s(0))
fibiter(b, c, x, y) → if(lt(c, b), b, c, x, y)
if(false, b, c, x, y) → x
if(true, b, c, x, y) → fibiter(b, s(c), y, plus(x, y))